$\forall$$M$:MsgA. Sends($M$) $\in$ $k$:Knd$\rightarrow$$M$.da($k$)$\rightarrow$$M$.state$\rightarrow$IdLnk$\rightarrow$($M$.Msg List)